package main;

import java.io.File;
import java.io.FileReader;
import java.util.ArrayList;
import java.util.Enumeration;
import java.util.Hashtable;

import javax.swing.JTextArea;
import javax.swing.SwingUtilities;

import lts.CompositeState;
import lts.LTSCompiler;
import lts.LTSException;
import lts.LTSInput;
import lts.LTSOutput;
import lts.SymbolTable;
import lts.ltl.AssertDefinition;
import main.LTSA.OutputAppend;
import main.LTSA.OutputClear;

public class LTSA implements LTSInput, LTSOutput {
	private int fPos = 0;
	private String fSrc = "\n";
	private JTextArea output = new JTextArea();
	private CompositeState current = null;
	private StringBuffer text;
	private ArrayList forSort;
	private String[] assert_names;

	public static void main(String args[]){
		/*LTSA main = new LTSA();
		main.parse();
		main.compileAll();*/
	}

	public LTSA(StringBuffer str) {
		SymbolTable.init();
		this.fPos = 0;
		this.fSrc = "\n";
		//this.output = new JTextArea();
		this.text = str;
		/*try {
			File file = new File ("output.lts");
			FileReader fr = new FileReader (file);
	        int c;
	        while((c=fr.read())!=-1){
	        	text.append((char)c);
	        }
	    }catch(Exception e){
	    	e.printStackTrace();
	    }*/
		this.fSrc = text.toString();
	}

	public void parse(){
		Hashtable cs1 = new Hashtable();
		Hashtable ps = new Hashtable();
		LTSCompiler comp = new LTSCompiler(this, this, "");
		comp.parse(cs1, ps);
		Enumeration e = cs1.keys();
		forSort = new ArrayList();
		while (e.hasMoreElements()) {
			forSort.add(e.nextElement());
		}
		AssertDefinition.compileAll(this);
	}
	
	public String[] getDefinitionArray(){
		return AssertDefinition.names();
	}
	
	public CompositeState runDefinition(String assertDefinition, LTSOutput output){
		return AssertDefinition.compile(output, assertDefinition);
	}
	

	public void compile(String name){
		fPos = -1;
		fSrc = text.toString();
		CompositeState cs = null;
		LTSCompiler comp = new LTSCompiler(this, this, "");
		cs = comp.compile(name);
	}

	public CompositeState docompile(String name){
		fPos = -1;
		fSrc = text.toString();
		CompositeState cs = null;
		LTSCompiler comp = new LTSCompiler(this, this, "");

		cs = comp.compile(name);
		return cs;
	}

	public void compileAll(){
		for(int i = 0; i<forSort.size();i++){
			this.docompile((String)forSort.get(i));
		}
	}

	public void safety(String name) {
		//compileIfChange();
		current = docompile(name);
		clearOutput();
		if (current != null) {
			current.analyse(this);
		}
	}

	public void safetyAll() {
		for(int i = 0; i<forSort.size();i++){
			this.safety((String)forSort.get(i));
		}
	}

	public void progress(String name) {
		clearOutput();
		current = docompile(name);
		if (current != null) {
			current.compose(this);
			current.checkProgress(this);
		}
	}

	public void progressAll() {
		for(int i = 0; i<forSort.size();i++){
			this.progress((String)forSort.get(i));
		}
	}
	
	public ArrayList getArrayModules(){
	    return forSort;
	}

	public String displayError(LTSException x) {
		String error = "";
		if (x.marker != null) {
			int i = ((Integer) (x.marker)).intValue();
			int line = 1;
			for (int j = 0; j < i; ++j) {
				if (fSrc.charAt(j) == '\n')
					++line;
			}
			error = "ERROR line:" + line + " - " + x.getMessage();
			outln(error);
			return error;
			//input.select(i, i + 1);
		} else{
			error = "ERROR - " + x.getMessage();
			outln(error);
			return error;
		}
	}

	class OutputAppend implements Runnable {
		String text;

		OutputAppend(String text) {
			this.text = text;
			System.out.print(text);
		}

		public void run() {
			output.append(text);
		}
	}

	class OutputClear implements Runnable {
		public void run() {
			output.setText("");
		}
	}

	class OutputShow implements Runnable {
		public void run() {
			System.out.println("swapto(1)");
			//swapto(1);
		}
	}

	public void out(String str) {
		SwingUtilities.invokeLater(new OutputAppend(str + ""));
	}

	public void outln(String str) {
		SwingUtilities.invokeLater(new OutputAppend(str + "\n"));
	}

	public void clearOutput() {
		SwingUtilities.invokeLater(new OutputClear());				
	}

	public char nextChar() {
		fPos = fPos + 1;
		if (fPos < fSrc.length()) {
			return fSrc.charAt(fPos);
		} else {
			// fPos = fPos - 1;
			return '\u0000';
		}
	}

	public char backChar() {
		char ch;
		fPos = fPos - 1;
		if (fPos < 0) {
			fPos = 0;
			return '\u0000';
		} else
			return fSrc.charAt(fPos);
	}

	public int getMarker() {
		return fPos;
	}
}
